This is TeX, WAITS Version 1.1 (preloaded format=cplain 84.8.28)  14 SEP 1984 14:59
**proofs.iii
(PROOFS.III[1,IAM] (CLTEX.FIX[TEX,CLT]) (BMAC.TEX[B2,JMC]) (BMAC.FIX[B2,JMC]
\sxfam=\fam11
)
\unit=\dimen18

[1]
Overfull \hbox (12.11229pt too wide) in paragraph at lines 13--16, p.3
\tenbf Base case: \tenrm Sup-pose that $\teni x$ \tenrm is an atom and $\teni y$
\tenrm ,$\teni ↑↑K \tensy 2 A \tenit l[]$ \tenrm are such that $[] [\teni x;  y;
  ↑↑K\tenrm ] \tensy 6\tenrm =|

\hbox(7.5+2.5)x361.34999, glue set - 1.0
.\tenbf B
.\tenbf a
.\tenbf s
.\tenbf e
.\glue 3.83333 plus 1.91666 minus 1.27777
.etc.

[2]
Overfull \hbox (6.50246pt too wide) in paragraph at lines 34--37, p.3
[]\tenrm In the sec-ond case, since $[] [\teni x;  y;  ↑↑K\tenrm ] \tensy 6\tenr
m = []$, we must have that $[] [\teni x;  y;  ↑↑K\tenrm ] =|

\hbox(7.5+2.5)x361.34999, glue set - 1.0
.\hbox(0.0+0.0)x20.0
.\tenrm I
.\tenrm n
.\glue 3.33333 plus 1.66666 minus 1.1111
.\tenrm t
.etc.

[3] [4] [5] [6] [7]
Overfull \hbox (17.74931pt too wide) in paragraph at lines 49--49, p.7
[]|\ninett (defun subsub (a b) (if (null a) a (cons (cons (caar a) (sublis (cdar
 a) b)) |

\hbox(8.0+3.0)x361.34999
.\hbox(0.0+0.0)x20.0
.\rule(8.0+3.0)x0.0
.\ninett (
.\ninett d
.\ninett e
.etc.

[8]
Overfull \hbox (8.29933pt too wide) in paragraph at lines 19--19, p.8
[]|        \ninett ((isvar x) (if (occur x y) 'no (compose a (cons (cons x y) ni
l)))) |

\hbox(8.0+3.0)x361.34999
.\hbox(0.0+0.0)x20.0
.\rule(8.0+3.0)x0.0
.\glue 4.72499
.\glue 4.72499
.\glue 4.72499
.etc.


Overfull \hbox (8.29933pt too wide) in paragraph at lines 20--20, p.8
[]|        \ninett ((isvar y) (if (occur y x) 'no (compose a (cons (cons y x) ni
l)))) |

\hbox(8.0+3.0)x361.34999
.\hbox(0.0+0.0)x20.0
.\rule(8.0+3.0)x0.0
.\glue 4.72499
.\glue 4.72499
.\glue 4.72499
.etc.

[9] [10] [11] [12] [13] [14] [15] [16]
Overfull \hbox (27.1993pt too wide) in paragraph at lines 12--12, p.13
[]|        \ninett ((isvar x) (if (v-occur x y a) 'no (compose a (cons (cons x y
) nil)))) |

\hbox(8.0+3.0)x361.34999
.\hbox(0.0+0.0)x20.0
.\rule(8.0+3.0)x0.0
.\glue 4.72499
.\glue 4.72499
.\glue 4.72499
.etc.


Overfull \hbox (27.1993pt too wide) in paragraph at lines 13--13, p.13
[]|        \ninett ((isvar y) (if (v-occur y x a) 'no (compose a (cons (cons y x
) nil)))) |

\hbox(8.0+3.0)x361.34999
.\hbox(0.0+0.0)x20.0
.\rule(8.0+3.0)x0.0
.\glue 4.72499
.\glue 4.72499
.\glue 4.72499
.etc.

[17] [18]
Output written on PROOFS.DVI[B2,JMC] (18 pages, 51280 bytes).